(declare-const v9 Bool)
(declare-const v10 Bool)
(declare-const v11 Bool)
(declare-const v12 Bool)
(declare-const v13 Bool)
(declare-const v14 Bool)
(declare-const v15 Bool)
(declare-const i0 Int)
(declare-const i4 Int)
(declare-const i6 Int)
(declare-const i7 Int)
(declare-const i9 Int)
(declare-const i11 Int)
(declare-const i12 Int)
(declare-const i17 Int)
(declare-const r0 Real)
(declare-const r4 Real)
(declare-const r7 Real)
(declare-const r8 Real)
(declare-const r10 Real)
(declare-const r11 Real)
(declare-const r13 Real)
(declare-const r14 Real)
(declare-const r16 Real)
(declare-const r17 Real)
(declare-const r18 Real)
(assert (exists ((q0 Real)) (= i7 i9)))
(declare-const v16 Bool)
(declare-const v17 Bool)
(declare-const r19 Real)
(declare-const _18-0 (_ BitVec 18))
(declare-const v18 Bool)
(declare-const v19 Bool)
(declare-const r20 Real)
(declare-const v20 Bool)
(declare-const i20 Int)
(declare-const r21 Real)
(assert (exists ((q1 (_ BitVec 5))) v20))
(declare-const i21 Int)
(declare-const v21 Bool)
(push)
(pop)
(push)
(assert (or (<= 6329 r4 r17 269846265) (is_int r4)))
(assert (or (is_int r4) v9 (<= 6329 r4 r17 269846265) (is_int r4) (<= 6329 r4 r17 269846265) v9 (is_int r4) v9 (is_int r4)))
(assert (or v9 (is_int r4)))
(assert (or v9 (<= 6329 r4 r17 269846265) v9 (<= 6329 r4 r17 269846265)))
(check-sat)
